Section: Scientific Foundations

Software infrastructure

The Sardes approach to software infrastructure is both architecture-based and language-based: architecture-based for it relies on an explicit component structure for runtime reconfiguration, and language-based for it relies on a high-level type safe programming language as a basis for operating system and middleware construction. Exploiting high-level programming languages for operating system construction [109] has a long history, with systems such as Oberon [113] , SPIN [60] or JX [74] . More recent and relevant developments for Sardes are:

• The developments around the Singularity project at Microsoft Research [72] , [80] , which illustrates the use of language-based software isolation for building a secure operating system kernel.

• The seL4 project [75] , [86] , which developed a formal verification of a modern operating system microkernel using the Isabelle/HOL theorem prover.

• The development of operating system kernels for multicore hardware architectures such as Corey [63] and Barrelfish [59] .

• The development of efficient run-time for event-based programming on multicore systems such as libasync [114] , [88] .